package at.fhj.ase;

public class Buffer implements Cloneable {

	protected int in,out;
	protected Object[] buf;

	public Buffer() {

		buf = new Object[0];
		/* invariant */
		jassCheckInvariant("at end of method Buffer().");
	}

	public Buffer (int anzahl) {

		/* precondition */
		if (!(anzahl>0)) throw new jass.runtime.PreconditionException("at.fhj.ase.Buffer","Buffer(int)",13,null);
		buf = new Object[anzahl];
		/* postcondition */
		if (!(buf.length==anzahl)) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","Buffer(int)",15,null);
		/* invariant */
		jassCheckInvariant("at end of method Buffer(int).");
	}

	public boolean empty() {		boolean jassResult;

		/* invariant */
		jassCheckInvariant("at begin of method empty().");
	at.fhj.ase.Buffer jassOld = (at.fhj.ase.Buffer)this.clone();
		jassResult = ( in - out == 0);
		/* postcondition */
		if (!(in == jassOld.in && out == jassOld.out && jass.runtime.Tool.arrayEquals(buf,jassOld.buf))) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","empty()",-1,"Method has changed old value.");
		/* invariant */
		jassCheckInvariant("before return in method empty().");
		return jassResult;
	}

	public boolean full() {		boolean jassResult;

		/* invariant */
		jassCheckInvariant("at begin of method full().");
	at.fhj.ase.Buffer jassOld = (at.fhj.ase.Buffer)this.clone();
		jassResult = ( in - out == buf.length);
		/* postcondition */
		if (!(in == jassOld.in && out == jassOld.out && jass.runtime.Tool.arrayEquals(buf,jassOld.buf))) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","full()",-1,"Method has changed old value.");
		/* invariant */
		jassCheckInvariant("before return in method full().");
		return jassResult;    
	}

	public void add(Object o) {

		/* invariant */
		jassCheckInvariant("at begin of method add(java.lang.Object).");
	at.fhj.ase.Buffer jassOld = (at.fhj.ase.Buffer)this.clone();
		/* precondition */
		if (!(o!=null)) throw new jass.runtime.PreconditionException("at.fhj.ase.Buffer","add(java.lang.Object)",29,"valid_object");
		if (!(!jassInternal_full())) throw new jass.runtime.PreconditionException("at.fhj.ase.Buffer","add(java.lang.Object)",29,"buffer_not_full");
		buf[in % buf.length] = o;
		in++;
		/* postcondition */
		if (!(jassOld.in==in-1)) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","add(java.lang.Object)",32,null);
		if (!(out == jassOld.out)) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","add(java.lang.Object)",-1,"Method has changed old value.");
		/* invariant */
		jassCheckInvariant("at end of method add(java.lang.Object).");
	}

	public Object remove() {		java.lang.Object jassResult;

		/* invariant */
		jassCheckInvariant("at begin of method remove().");
	at.fhj.ase.Buffer jassOld = (at.fhj.ase.Buffer)this.clone();
		/* precondition */
		if (!(!jassInternal_empty())) throw new jass.runtime.PreconditionException("at.fhj.ase.Buffer","remove()",36,"buffer_not_empty");
		Object o = buf[out % buf.length];
		out++;
		jassResult = ( o);
		/* postcondition */
		if (!(jassResult!=null)) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","remove()",40,"valid_object");
		if (!(in == jassOld.in && jass.runtime.Tool.arrayEquals(buf,jassOld.buf))) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","remove()",-1,"Method has changed old value.");
		/* invariant */
		jassCheckInvariant("before return in method remove().");
		return jassResult;
	} 

	public boolean contains(Object o) {		boolean jassResult;

		/* invariant */
		jassCheckInvariant("at begin of method contains(java.lang.Object).");
	at.fhj.ase.Buffer jassOld = (at.fhj.ase.Buffer)this.clone();
		/* precondition */
		if (!(o!=null)) throw new jass.runtime.PreconditionException("at.fhj.ase.Buffer","contains(java.lang.Object)",44,null);
		boolean found = false;
		{
			int jassVariant;
			int i = 0;
			for (jassCheckLoop(0<=i&&i<=buf.length,new jass.runtime.LoopInvariantException("at.fhj.ase.Buffer","contains(java.lang.Object)",47,null))
			,jassVariant=buf.length-i,jassCheckLoop(jassVariant>=0,new jass.runtime.LoopVariantException("at.fhj.ase.Buffer","contains(java.lang.Object)",48,"Loopvariant is below zero."))
			; i < buf.length;
			 i++,jassCheckLoop(0<=i&&i<=buf.length,new jass.runtime.LoopInvariantException("at.fhj.ase.Buffer","contains(java.lang.Object)",47,null))
			,jassCheckLoop(jassVariant>buf.length-i,new jass.runtime.LoopVariantException("at.fhj.ase.Buffer","contains(java.lang.Object)",48,"Loopvariant was not decreased.")),jassVariant=buf.length-i
			,jassCheckLoop(jassVariant>=0,new jass.runtime.LoopVariantException("at.fhj.ase.Buffer","contains(java.lang.Object)",48,"Loopvariant is below zero."))
			)
				if (buf[i].equals(o)) 
					found = true;
		}
		jassResult = ( found);
		/* postcondition */
		if (!(in == jassOld.in && out == jassOld.out && jass.runtime.Tool.arrayEquals(buf,jassOld.buf))) throw new jass.runtime.PostconditionException("at.fhj.ase.Buffer","contains(java.lang.Object)",-1,"Method has changed old value.");
		/* invariant */
		jassCheckInvariant("before return in method contains(java.lang.Object).");
		return jassResult;    
	}   

	protected Object clone() {		java.lang.Object jassResult;

		/* invariant */
		jassCheckInvariant("at begin of method clone().");
		/* Use the Objects clone method. This is enough cause only in and out 
		       are refered with Old expressions. */
		Object b = null;
		try {
			b = super.clone();
		}     
		catch (CloneNotSupportedException e){;}
		jassResult = ( b);
		/* invariant */
		jassCheckInvariant("before return in method clone().");
		return jassResult;
	}

	/* --- The following methods of class at.fhj.ase.Buffer are generated by JASS --- */


	public boolean jassInternal_full() {
		return in - out == buf.length;    
	}


	public boolean jassInternal_empty() {
		return in - out == 0;
	}

	private boolean jassInternal_checkingInvariant = false;
	private void jassCheckInvariant(String msg) {
		if(jassInternal_checkingInvariant) return;
		jassInternal_checkingInvariant = true;
		if (!(0<=in-out&&in-out<=buf.length)) throw new jass.runtime.InvariantException("at.fhj.ase.Buffer",null,66,"Exception occured "+msg+" (range)");
		if (!(buf.length==0||(jassCheckForAll_0_at_fhj_ase_Buffer()))) throw new jass.runtime.InvariantException("at.fhj.ase.Buffer",null,67,"Exception occured "+msg+" (valid_content)");
		jassInternal_checkingInvariant = false;
	}

	private final void jassCheckLoop(boolean b, jass.runtime.AssertionException e) {
		if(!b) throw e;
	}

	protected final boolean jassCheckForAll_0_at_fhj_ase_Buffer() {
		try {
			int i;
			for(i = out%buf.length;i <= in%buf.length-1;i++) {
				if (!(buf[i]!=null)) return false;
			}
			return true;
		}
		catch (ArrayIndexOutOfBoundsException jassException) {
			throw new jass.runtime.AssertionException("at.fhj.ase.Buffer",null,68,"Arraybounds in forall/exists expression violated ! ("+jassException.toString()+")");
		}
	}

}
